Nuprl Lemma : assert_of_set_leq 13,42

p:PosetSig, a, b:|p|. ((a () b)) = (a  b)   
latex


Upsets 1
Definitions of Statementa  b
Definitionst  T, a  b, x f y, , x:A. B(x)
Lemmasposet sig wf, set car wf, set le wf, assert wf

origin